LAp (LAp A) = LAp A by ROUGHS_1:33;
hence LAp A is open by OpIsLap; :: thesis: verum