let X, Y be Subset of CQC-WFF ; :: thesis: for p being Element of CQC-WFF st X |- p & X c= Y holds
Y |- p
let p be Element of CQC-WFF ; :: thesis: ( X |- p & X c= Y implies Y |- p )
assume A1: ( X |- p & X c= Y ) ; :: thesis: Y |- p
then consider f being FinSequence of CQC-WFF such that
A2: ( rng f c= X & |- f ^ <*p*> ) by HENMODEL:def 2;
rng f c= Y by A1, A2, XBOOLE_1:1;
hence Y |- p by A2, HENMODEL:def 2; :: thesis: verum